$\forall$${\it left}$, ${\it right}$:Realizer. (${\it left}$ $\oplus$ ${\it right}$) $\in$ Realizer